feat: add optimization constants #1899
Conversation
felixpernegger
changed the title
|
|
||
| namespace Constant1a | ||
|
|
||
| /-- A real number satisfying a certain inequality about integral. -/ |
There was a problem hiding this comment.
I think this docstring could be a little more descriptive:)
There was a problem hiding this comment.
Thanks, I updated the docstring. I hope its better now.
I dont think putting the entire inequality in the docstring makes sense though as its quite technical.
|
|
||
| /-- How can the upper bound be improved? -/ | ||
| @[category research open, AMS 05 11 26] | ||
| theorem c1a_le : C1a ≤ answer(sorry) := by |
There was a problem hiding this comment.
| theorem c1a_le : C1a ≤ answer(sorry) := by | |
| theorem c1a_le : ∃ (c : ℝ), c < 1.5029 ∧ C1a ≤ c := by |
Might be a version without answer(sorry) or
theorem c1a_le : ∃ (c : ℝ), c = answer(sorry) ∧ c < 1.5029 ∧ C1a ≤ c := byhas the advantage, that no manually check is needed if a good answer was found.
I think it would be worth the effort to think about how to best do this if we are doing this for many optimization problems!
Perhaps we could add some definitions that work analogously.
Pinging also @Paul-Lez and @YaelDillies and @smmercuri and @callesonne and @eric-wieser
for ideas.
Here's an adhoc way I did it at the time: this is https://teorth.github.io/optimizationproblems/constants/1b.html
(probably needs update of the constants, btw)
formal-conjectures/FormalConjectures/ErdosProblems/36.lean
Lines 181 to 209 in 169aaeb
This is also a thing to consider: we might want to introduce a mechanism to pull the constants from
https://teorth.github.io/optimizationproblems/constants
So perhaps they better go into an attribute?
3 participants
See the discussion at
https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Optimization.20constants/with/570016079
It is probably useful if there is a somewhat standard way to phrase the open question (what is lower and upper bound etc) and this is likely a good place to discuss this. Namely how many of the theorems/conjectures
c1a_le,c1a_ge,c1a_eqdo we want etc?(Maybe also add optimization constants to the readme, next the green and erdos problems? as well as a tag for PRs)
Once/If this PR is merged, I will try to make the optimization constants repository link to this, similar as it is done for Erdos problems.